package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class Choose {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Choose");
		 
		 //Clocks
		 tiosts.addClock("clockC");
		 
         // Variables
         TypedData optionC = new TypedData("optionC", Constants.TYPE_INTEGER);
         tiosts.addVariable(optionC);
         
         // Parameters
         TypedData op = new TypedData("op", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(op);
         
         // Input, output, and internal actions
         Action init = new Action("initC", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
         Action select = new Action("select", Constants.ACTION_INPUT);
         select.addParameter(op.getName());
         tiosts.addAction(select);
         Action returnAction = new Action("return", Constants.ACTION_OUTPUT);
         tiosts.addAction(returnAction);
         Action performPayment = new Action("performPayment", Constants.ACTION_OUTPUT);
         tiosts.addAction(performPayment);
         Action shutdown = new Action("shutdown", Constants.ACTION_OUTPUT);
         tiosts.addAction(shutdown);
         Action send = new Action("send", Constants.ACTION_OUTPUT);
         send.addParameter(op.getName());
         tiosts.addAction(send);
         
         // Locations
         Location start = new Location("StartC");
         tiosts.addLocation(start);
         Location s0 = new Location("S0");
         tiosts.addLocation(s0);
         Location s1 = new Location("S1");
         tiosts.addLocation(s1);    
         Location s2 = new Location("S2");
         tiosts.addLocation(s2);  
         Location s3 = new Location("S3");
         tiosts.addLocation(s3);  
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("StartC", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S0");
         tiosts.createTransition("S0",  Constants.GUARD_TRUE, Constants.GUARD_TRUE, select, "optionC := op", null, Constants.DEADLINE_LAZY, "S1");
         //cash = 1   card = 2  check = 3 off = 4
         tiosts.createTransition("S1",  "optionC = 1 OR optionC = 2 OR optionC = 3", "clockC <= 10", performPayment, null, null, Constants.DEADLINE_LAZY, "S2");
         tiosts.createTransition("S1",  "optionC = 4", "clockC <= 10", shutdown, null, null, Constants.DEADLINE_LAZY, "S2");
         tiosts.createTransition("S1",  Constants.GUARD_TRUE, "clockC > 10", returnAction, null, "clockC := 0", Constants.DEADLINE_LAZY, "S0");
         tiosts.createTransition("S2", "optionC = op", Constants.GUARD_TRUE, send, null, null, Constants.DEADLINE_LAZY, "S3");
         
         return tiosts;		 
	 }

}
